Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.415.52, 004.434
Номер:6 (158)
Скачать PDF0 Кбайт
Язык спецификации взаимодействия автоматных объектов
Аннотация:
Введение. Автоматное программирование — парадигма программирования, успешно применяемая при разработке реагирующих систем, распределенных систем управления и различных ответственных приложений, где критически важна возможность верификации соответствия реальной системы ее модели, заданной в виде спецификаций. Традиционное тестирование таких систем может быть затруднено, поэтому требуются более совершенные средства верификации для повышения степени доверия к надежности реальной системы. Предложенный ранее язык спецификации кооперативного взаимодействия автоматных объектов (Cooperative Interaction of Automata Objects, CIAO) был успешно применен для разработки нескольких реагирующих систем. Однако он также выявил ряд недостатков, которые устранены в CIAO v.3. Метод. Новая версия языка разработана с целью автоматической верификации автоматных программ по формальным спецификациям определенного класса систем реального времени. CIAO v.3 содержит три нововведения в отличие от предшествующих версий. Во-первых, явное разграничение автоматных классов и автоматных объектов как экземпляров этих классов. Во-вторых, спецификация связывания автоматных объектов через интерфейсы с помощью схемы связей. В-третьих, описание семантики поведения системы взаимодействующих автоматных объектов с помощью семантического граф а. Основные результаты. В работе представлены основные концепции новой версии языка, приведены абстрактный синтаксис, операционная семантика и метамодель. Обсуждение. CIAO v.3 позволяет естественным образом включить в парадигму автоматного программирования почти все преимущества объектноориентированного программирования. Подключение автоматных объектов через соответствующие интерфейсы произвольным образом отражает схема связей. Семантический граф, описывающий семантику поведения автоматной программы, используется для реализации автоматической верификации относительно некоторых формальных спецификаций.
Ключевые слова:
Постоянный URL
Статьи в номере
- Разработка и изготовление коллимирующей волоконной сферической микролинзы для системы вывода излучения из радиофотонных компонент в оптическое волокно
- От триасового периода к современности: спектроскопия комбинационного рассеяния света для дифференциации ископаемых смол различного возраста
- Оптимизация геометрии двумерного фотоннокристаллического волновода для телекоммуникационных применений и сенсорики
- Разработка и исследование способов подавления аддитивных шумов в волоконнооптических интерферометрических датчиках
- Методика компенсации постоянной составляющей шумов рефлектограммы волоконно-оптической линии связи в условиях недостаточного динамического диапазона оптического рефлектометра обратного рассеяния во временной области
- Исследование метода измерения веса подвижных объектов на основе квазираспределенных волоконных решеток Брэгга с температурной компенсацией
- Современные оптические методы бесконтактных геометрических измерений и восстановления 3D-формы поверхности объектов: обзор
- Спектрально-люминесцентные свойства серебряных кластеров Ag1–5 в ионообменном слое силикатного стекла
- Формирование толстого слоя ε-Ga2O3 на подслое GaN с V-дефектами на границе раздела
- Модель обеспечения непрерывности безопасного функционирования системы прослеживаемости качества продукции в условиях неустойчивой коммуникации
- Применение марковских цепей Монте-Карло и машинного обучения для поиска активного модуля в биологических графах
- Обнаружение дефектов твердых поверхностей при ограниченном объеме данных на основе SSD-детектора и сиамских сетей
- Анализ настроений арабских твитов с использованием контролируемого машинного обучения
- Параметрический корпус русского языка RuParam
- Сравнительный анализ сгенерированных и оригинальных аннотаций научных статей по филологической тематике
- Повышение безопасности Kubernetes с помощью машинного обучения: проактивный подход к обнаружению аномалий
- Многозадачное обучение на основе префиксов для устойчивого текстового поиска
- Улучшение вопросно-ответных систем в области программирования с дообучением языковых моделей на структурированных разнородных данных онлайн-форумов
- Особенности организации игрового взаимодействия асимметричных агентов с использованием графовых нейронных сетей
- Разработка и моделирование технологической схемы установки паровой конверсии метана с кислородным сжиганием топлива и улавливанием углекислого газа
- Исследование стабильности гибридной МОП-мемристорной памяти с использованием модифицированного метода оптимизации роя частиц
- Анализ уязвимости нейросетевых моделей YOLO к атаке Fast Sign Gradient Method